%\documentclass[a4paper,10pt]{article}
\documentclass[envcountsect,envcountsame,runningheads,a4paper]{llncs} 
% \documentclass[runningheads,a4paper]{llncs}


\usepackage[utf8]{inputenc}

\usepackage[english]{babel}
\usepackage{xspace}
\usepackage{float}
\usepackage{mathpartir}

\usepackage{amstext, amssymb, amsfonts, amsmath}
\usepackage{latexsym}
\usepackage{stmaryrd}
\usepackage{float}
\usepackage{graphicx}
\usepackage{enumerate}
\usepackage{times}
\usepackage{color}
\usepackage{url}
\usepackage{hyperref}
\usepackage{proof}

\usepackage{macron}
\usepackage{typecasemacro}


\usepackage{lineno}
\linenumbers

\newtheorem{newnotation}[theorem]{Notation}


%opening
\title{
Runtime Adaptation in Communication-Centric Systems: An Event-Based Approach
%An Event-Based Architecture for Runtime Adaptation in Communication-Centric Systems
}
\author{Cinzia Di Giusto \inst{1} \and Jorge A. P\'{e}rez\inst{2}}
\institute{%Universite d'Evry 
Universit\'{e} d'Evry - Val d'Essonne, Laboratoire IBISC, Evry, France
\and CITI and Departamento de Inform\' atica, FCT, Universidade Nova de Lisboa, Portugal }



\begin{document}

\maketitle



     
\begin{abstract}
%Modern distributed software systems are \emph{communication-centric}: 
%built as assemblies of software artifacts, 
%these systems rely on consistent dialogues among such artifacts. 
%Ensuring that such dialogues conform to
%their prescribed protocols is thus key to correctness.
% As  systems become more complex, correctness analyses must unavoidably 
% account for issues not strictly tied to communication but that influence overall   behavior.
% This paper deals with one of such issues,
% \emph{runtime adaptation},  here understood as the dynamic update of the behavior of part of the system.
%We offer two main contributions
%on the integration of runtime adaptation into \emph{session types} for structured communications.
%First, we propose an \emph{event-based}  
%approach to 
%runtime adaptation
%of session typed processes: by 
%relying on selected features from  
%the eventful session framework by Kouzapas et al, we are able to 
%define rich forms of adaptation, 
%even for processes with active running sessions.
%Second,
%we propose a simple architecture for communication-centric systems with runtime adaptation. 
%By formalizing \emph{compartmentalized} communications, 
%our architecture offers  an alternative for organizing session-based systems and services.

Modern distributed software systems are \emph{communication-centric}: 
built as assemblies of software artifacts, 
these systems rely on consistent dialogues among such artifacts. 
Ensuring conformance of these dialogues to prescribed protocols is thus key to correctness.
 As  systems become more complex, correctness analyses must unavoidably 
 account for issues not strictly tied to communication but that influence overall   behavior.
 This paper deals with one of such issues,
 \emph{runtime adaptation},  here understood as the dynamic update of the behavior of part of the system.
Concretely, we are interested in integrating mechanisms for runtime adaptation into \emph{session types} for structured communications.
We offer two main contributions.
First, 
%we propose an \emph{event-based}  approach to runtime adaptation of session typed processes: 
by  relying on selected features from  
the eventful session framework by Kouzapas et al, 
we propose an \emph{event-based}  approach to runtime adaptation of session typed processes.
Our approach enables us to 
%we are able to 
define rich forms of adaptation, 
even for processes with active running sessions.
Second,
we propose a simple architecture for communication-centric systems with runtime adaptation. 
By formalizing \emph{compartmentalized} communications, 
our architecture offers  an alternative for organizing session-based systems and services.

\end{abstract}
%
%\section{Suggestions}
%%The abstract can be much shorter and more general. 
%
%Mention the well-known work on exceptions for binary session types, and other session disciplines with buffers/queues~\cite{DBLP:journals/jfp/GayV10}.
%
%Before giving technical details, it would be very useful to give a concrete example for configurations/networks, and their evolution.
%The example could illustrate records, memories, etc. 


\section{Introduction}
Modern distributed %software 
systems are \emph{communication-centric}: 
built as assemblies of software artifacts, 
these systems rely on consistent dialogues among such artifacts. 
Ensuring conformance of these dialogues to prescribed protocols is key to correctness.
In \emph{session-based concurrency},  
 dialogues are structured into %basic 
 units called sessions; interaction patterns are abstracted as \emph{session types}~\cite{DBLP:conf/esop/HondaVK98}, 
against which specifications may be checked. 

This paper addresses the challenge of integrating mechanisms for \emph{runtime adaptation} 
into a %typed 
model of session-based concurrency.
We build upon our prior work~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}, which 
proposed the typeful integration of two basic adaptation mechanisms.
In this paper, 
we (i)~refine and enhance such mechanisms, and also  
(ii)~clarify their status within formal models of session-based communication.
A distinctive feature of the present development is that we follow an \emph{event-based} approach, relying on constructs from~\cite{Kouzapas12,KouzapasJ13}. 
 
As communication-centric systems are inherently open, and  operate on highly dynamic infrastructures, 
\emph{runtime adaptation} appears as an essential feature to ensure continued system operation %, optimize costs, 
and enhance business agility.
As in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}, 
%in this paper 
here we understand runtime adaptation as the dynamic modification of (the behavior of) the system as a response to an exceptional  \emph{event}, not necessarily catastrophic. Formal specification(s) of the system should describe the sub-systems amenable to adaptation and their exceptional events. 
%Then, on the basis of an initial specification and its projected evolution, an array of potential adaptation routines is defined at design time. 
In this context, integrating runtime adaptation mechanisms into session-based concurrency is a challenging problem: although runtime adaptation
is not strictly tied to communication it may influence overall behavior.
Hence, formal integrations require a delicate balance between the two intertwined concerns of structured communications and 
runtime adaptation.
 
To realize 
this integration,
the approach that we have pursued in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}  relies on 
%To integrate this vision of runtime adaptation into a session typed process language, i we have appealed to 
the two key constructs of the \emph{adaptable processes} framework~\cite{BGPZFMOODS}.
Given a location $\locf{loc}$ (a distinguished computation site), a process $P$, and a context $Q(\mathsf{X})$ 
(a process with zero or more occurrences of process variable $\mathsf{X}$),
the framework in~\cite{BGPZFMOODS} introduces 
so-called \emph{located processes} and \emph{update processes}, written $\scomponent{\locf{loc}}{P}$ and 
$\nadapt{\locf{loc}}{Q(\mathsf{X})}$, respectively.
These two processes may synchronize on $\locf{loc}$; by doing so, one obtains process 
$Q\subst{P}{\mathsf{X}}$, i.e. the process $Q$ in which all free occurrences of $\mathsf{X}$ are replaced with $P$.
This step represents the \emph{update} of  process $P$ at $\locf{loc}$ with an \emph{adaptation routine}
embodied by $Q$. Locations can be nested and are transparent:
within $\scomponent{\locf{loc}}{P}$, process $P$ may evolve autonomously, with the potential of interacting with some 
update process for $\locf{loc}$. 

Combining located and update processes gives an expressive alternative for specifying 
runtime adaptation for communicating processes. %, in the sense defined above,  for .
In~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13} we have integrated 
these two constructs into a session-typed $\pi$-calculus. 
To address the desired balance between communication and adaptation concerns, 
%in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13} 
we have proposed the \emph{consistency} property: 
 update actions over located processes which are engaged in active session behavior cannot be enabled. 
 Intuitively, this means that adaptation actions do not jeopardize already established sessions.
Via the novel notion of \emph{session interface}, the technical machinery used to enforce consistency guarantees also the preservation of locations enclosing service definitions: this ensures, e.g.,
 that a public persistent session server %, possibly useful to different clients at different times, 
 is never discarded as a result of an update step.
 The session type system in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13}
 ensures both safety (i.e., absence of communication errors at runtime) and consistency.

%\newpage
\noindent While intuitive, the mechanisms introduced in~\cite{DBLP:conf/sac/GiustoP13,DBLP:journals/corr/GiustoP13} are limited in two ways:
\begin{enumerate}[1.]
\item As detailed above, an adaptation step may take place when a located process and an update process can synchronize on some location. As such, specifying the precise moment in which such a step should occur can be sometimes difficult, for one must explicitly embed located and update processes within communication prefixes. This overly explicit specification of adaptation routines is well-suited to specify \emph{internal adaptation requests} (i.e., requests issued by the system itself) but turns out to be inadequate to specify \emph{external adaptation requests}, i.e., requests communicated to the system by its environment.
%This suggest that our existing mechanisms could be improved by an 
This suggests the need for an %What seems to be required to enhance our mechanisms is an
orthogonal communication layer which treats internal and external adaptation requests in a uniform manner.

\item Consistency may sometimes be overly protective.
Consider  relocation-based adaptation, in which the active communication behavior in some location is moved unchanged to some other location. While  conceptually simple, this form of adaptation is precluded by our notion of consistency: adaptation is blocked as long as the original location contains active sessions. This may be problematic: in some settings, forcing a relocation to occur only upon session completion may even defeat its purpose. 
Rather than forbidding adaptation steps over locations with active sessions, a more sophisticated mechanism could enable only those steps which preserve such active sessions. This suggests the need for ways of tracking the state of the sessions (protocols) running in any given location; this would allow to assess whether potential adaptation routines preserve such state or not. 
\end{enumerate}

\noindent To address the two needs above, we propose to appeal to constructs included in the \emph{eventful} session types framework developed by Kouzapas et al~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}. In fact, 
such a framework allows for non-blocking detection of event/message arrivals (as required by (1) above), 
and defines the dynamic inspection of session types (as required by (2) above). A first main contribution of this paper is the enhancement of our approach to runtime adaptation %of session-typed processes 
with these two event-based mechanisms.
%integrating these elements of the eventful session framework into our own . We highlight key aspects of this integration:
Key novelties include:
\begin{enumerate}[i.]
\item We treat adaptation requests, both internal and external, as messages. Each location is associated to a queue which stores adaptation requests. One could then use the message detector mechanisms of the eventful session framework to specify adaptation managers which are triggered when an adaptation request arrives. As queues are associated to locations but are independent from the communication behaviors enclosed in them, such queues could serve as an interface between the system and its environment. Also, as the message detector can check for certain messages, one can specify adaptation managers dedicated to particular kinds of requests.

\item We enhance update processes with the ability of dynamically inspecting the session types active in a given location.
This is useful to assess the suitability of adaptation routines at runtime. This enhancement relies on two elements: the first is a queue that contains the type associated to each active session; the second is a generalized form of the $\mathsf{typecase}$ construct, which is able to ``test'' the state of a finite number of active sessions prior to enable an adaptation step. Using these enhanced update processes, adaptation routines may have an effect on locations with open sessions. 
\end{enumerate}
\noindent By combining (i) and (ii) above, we obtain a rich framework for specifying and reasoning about runtime adaptation. 
The resulting framework, presented and developed in \S\,\ref{s:evadap}, enjoys communication safety. 
To the best of our knowledge, eventful session constructs have not been exploited for specifying and reasoning about runtime adaptation issues; the framework we present here thus constitutes an original application for them. 

Having introduced an eventful framework for runtime adaptation of located session typed processes, several natural questions arise.
For instance, given that adaptation requests are handled at the level of locations, how should be processes organized into such locations to achieve coherent adaptation strategies? Also, would it be possible to structure the event- and adaptation-related elements of the framework in~\S\,\ref{s:evadap} in such a way that the separation between communication and adaptation concerns is made explicit? 

To address this issue, our second main contribution is a \emph{compartmentalized} model for communication-centric applications.
This model, described in~\S\,\ref{s:arch}, is intended to be a reference for organizing the elements of the framework in~\S\,\ref{s:evadap} into modular units of communication and runtime adaptation. It enforces the separation between communication behavior, event-related elements (e.g., queues), and adaptation constructs. Rather than a fully defined architectural model, our compartmentalized model is meant to serve as a simple but compelling illustration of (a)~how session process specifications can be expressed and reasoned about at higher level of abstraction, and (b)~how define interaction between constructs for communication, state, and adaptation while keeping formal and conceptual separations between the three. We define formal syntax and semantics for specifications of the compartmentalized model, and informally argue that the static analysis techniques available for the ``plain'' processes of~\S\,\ref{s:evadap} scale to compartmentalized processes. 

\subsubsection*{Related Work}
The first papers on eventful sessions, including theory and implementation aspects, are \cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11}; their associated journal paper is~\cite{KouzapasJ13}. The PhD thesis of Kouzapas~\cite{Kouzapas12} provides a unified presentation. 


%\section{Motivation}
%%Before introducing the architecture, which is a conceptual contribution, we should detail 
%We now motivate how the asynchronous framework for eventful sessions of~\cite{Kouzapas12} 
%offers a good basis for specifying runtime adaptation for session-typed processes with running sessions. 
%%This is a simple technical contribution; it is desirable to understand well these technical issues before building a whole architecture upon them.
%In the rest of this section, we assume 
%the syntax, semantics, and typing system of~\cite{Kouzapas12}.
%
%\subsection{Updating Processes With Open Sessions I: Queues}
%What we borrow from that framework in~\cite{Kouzapas12} is actually only a few things: 
%(i)~their use of the current state of a session, recorded in an associated queue; 
%(ii)~their use of subtyping inside the reduction semantics.
%
%We add to the syntax of~\cite{Kouzapas12} two constructs:
%located processes, denoted $\scomponent{\locf{loc}}{P}$, and update actions, written $\nadapt{\locf{loc}}{Q(\til{z}{:}\til{\ST})}$.
%Located processes are as usual. The update action $\nadapt{\locf{loc}}{Q(\til{z}{:}\til{\ST})}$ acts on location $\locf{loc}$
%and contains an adaptation routine $Q$ (a process, not a context) 
%with open sessions $z_1:\ST_1, \ldots, z_n:\ST_n$. %, which implement sessions $\ST_1, \ldots, \ST_n$, respectively.
%We assume that $\mathsf{fc}(Q) = \til{z}$.
%
%
%In~\cite{Kouzapas12}, a queue associated to session $s$ is written $s[S, \mathsf{i}:\overline{h}, \mathsf{o}:\overline{h'}]$. 
%Here, %as we have ran out of symbols, 
%we write $\que{k}{\ST; M}$, where $\ST$ is the current session type for session $k$, with input and output messages $M$. 
%We now extend the reduction semantics of~\cite{Kouzapas12} so as to allow runtime adaptation.
%\begin{equation}\label{eq:redsem}
%\frac{
%\mathsf{fc}(P) = \til{\kappa} \quad 
%\rho = \subst{\til{\kappa}}{\til{z}} \quad
%\til{\STT} \leq \til{\ST} \qquad 
%\mathcal{S}(\til{\ST}) = \que{\kappa^p_1}{\ST_1; M_1} \para \dots \para \que{\kappa^p_n}{\ST_n; M_n}
%}{
%\scomponent{\locf{loc}}{P} \para
%\mathcal{S}(\til{\ST}) \para
%\nadapt{\locf{loc}}{Q(\til{z}{:}\til{\ST})}
%\pired 
%\scomponent{\locf{loc}}{\rho(Q)} \para \mathcal{S}(\til{\ST})
%}
%\end{equation}
%This is of course a very simple form of adaptation; still, it captures the essence of the update of a process
%with active sessions:
%\begin{enumerate}[1.]
%\item It does not involve the location $l$. Relocation is not admitted, so the location hierarchy is not disrupted. (Relocation is not particularly dangerous, but philosophically we seek updates that are as preserving as possible; in that line, preservation of location hierarchy seems reasonable.)
%\item It may handle the case in which $P$ has more than one active session
%\item It offers a new implementation for the location $l$, which is identical or better than the current one (up to subtyping)
%\item The state of the located process is preserved (or improved, thanks to subtyping)
%\end{enumerate}
%
%A drawback of this form of adaptation is that there is little control on \emph{when} an adaptation routine (update process) is made available.
%Some alternatives include, for instance, placing it within an if-then-else construct or after a given prefix. 
%These alternatives are internal, in the sense that they must be programmed (i.e., specified) in advance; the possibility of 
%external calls to adaptation routines (say, from a neighboring system not specified) is not present.
%In the following, we explore how to use events to govern the actual availability of adaptation routines.
%
%\subsection{Updating Processes With Open Sessions II: Adding Events}
%The drawback suggested before motivates the use of events for handling adaptation requests.
%We will now assume that locations $l$ will have an associated queue in which requests can be accumulated. 
%Then, by using the $\mathtt{arrive}$ predicate introduced in~\cite{Kouzapas12} within if-then-else expressions, we may 
%spawn the adaptation routine. This means that a possible template for adaptation routines for location $l$ could be the following:
%$$
%M = \mu X.\mathsf{if}~\arrive{l, adp}~\mathsf{then}~l\{Q(\til{z}:\til{\STT})\}~\mathsf{else}~X 
%$$
%with the intuitive meaning: if an adaptation event `$adp$' is detected as present in the queue of location $l$, then 
%spawn an update process; otherwise, if such an event is not detected, recurse.
%
%Notice that by appealing to queues, we can handle both internal and external adaptation requests: 
%as elements of the queue of $l$ are simply detected by $M$, independently of their origin, the associated update prefix
%can be released uniformly. One may also define a class of possible messages for that queue, in order to recognize whether requests are internal or external.
%For instance, we may define $\mathtt{arrive}(l\, int-adp)$ and $\mathtt{arrive}(l\, ext-adp)$.
%This refinement of the $\mathtt{arrive}$ predicate is simple to achieve and can add expressiveness.
%
%A drawback of this form of adaptation is the following.
%Notice that there could be interleaved actions between the moment in which the adaptation request is placed in a queue, 
%and the moment in which the update prefix is actually released. 
%In particular, it could occur that an update prefix that is appropriate for $l$ when the request is detected, 
%is no longer appropriate when the update prefix is ready to interact. A simple solution is to add a form of \emph{stopping}
%a location as soon as the adaptation event is detected. Precisely, we could 
%add a new prefix $\mathsf{stop}\, l$ to the language, with the following associated reduction rule
%$$
%l[P] \parallel \mathsf{stop}\, l;Q \pired l[\![P]\!] \parallel Q
%$$
%where $ l[\![P]\!]$ intuitively represents a located process in which $P$ can no longer evolve. 
%(These stopped located processes would only arise at runtime.)
%One would then re-define rule \eqref{eq:redsem} in terms of stopped located processes. 
%Finally, by defining 
%$$
%M' = \mu X.\mathsf{if}~\mathtt{arrive}(l\, adp)~\mathsf{then}~\mathsf{stop}\, l; l\{Q(\til{z}:\til{\STT})\}~\mathsf{else}~X 
%$$
%we could reduce the possibilities that the located process at $l$ modifies its sessions prior to 
%the release of the adaptation routine. %, thus ruling out potential adaptation routines.
%
%\subsection{Updating Processes With Open Sessions II: Adding Typecase}
%Although the use of events brings uniformity to adaptation, by itself it is not very precise.
%In fact, even with the addition of the $\mathsf{stop}$ prefix we could find discrepancies between 
%the issue of an adaptation request and the associated response offered by processes such as $M$ and $M'$.
%What we require is a mechanism which handles adaptation with the actual current state of all the sessions enclosed by a location.
%
%In~\cite{Kouzapas12}, the authors introduce a \emph{session typecase} operator, written 
%$$\mathsf{typecase}\,k\,\mathsf{of}\,\{(x_i : S_i) : P_i\}$$
%Informally, this operator  
%attempts to match the current (i.e. run-time) session type of channel $k$ 
%against the specified session types $S_i$, proceeding to the $P_i$ for the first $S_i$ that matches.
%We propose to modify this operator in two ways. First, 
%we generalize it so as to consider more than one session.
%The typecase would then consider the combination of the state of two or more sessions.
%Second, we embed it within update processes. The result is the following \emph{typeful update prefix}:
%$$l\big\{\mathsf{case}\,k_1,\ldots,k_n\,\mathsf{of}\,\{(x_{1i} : \ST_{1i}; \cdots; x_{ni} : \ST_{ni}) : Q_i\} \big\}$$
%which we abbreviate as 
%$$l\big\{\mathsf{case}\,\overline{k}\,\mathsf{of}\,\{(\overline{x_{i} : \ST_{i}}) : Q_i\} \big\}$$
%We may then re-define  rule \eqref{eq:redsem} as follows (roughly, some details to be checked):
%\begin{equation}\label{eq:redsem2}
%\frac{
%fc(P) = \til{\kappa} \quad 
%\rho = \subst{\til{\kappa}}{\til{z}} \quad
%\til{\STT} \leq \til{\ST} \qquad 
%\mathcal{S}(\til{\ST}) = \kappa_1\lfloor \ST_1; M_1 \rfloor \parallel \dots \parallel \kappa_n\lfloor \ST_n; M_n \rfloor
%}{
%l[P] \parallel 
%\mathcal{S}(\til{\ST}) \parallel
%%l\{Q(\til{z}:\til{\STT})\}
%l\big\{\mathsf{case}\,\overline{\kappa}\,\mathsf{of}\,\{(\overline{z_{i} : \STT_{i}}) : Q_i\} \big\}
%\pired 
%l[\rho(Q_k)] \parallel \mathcal{S}(\til{\ST})
%}
%\end{equation}
%where $Q_k$ is the adaptation behavior that is associated to a good match for all the $n$ sessions involved.
%Then, by appealing to events, we could define
%$$
%M'' = \mu X.\mathsf{if}~\mathtt{arrive}(l\, adp)~\mathsf{then}~l\big\{\mathsf{case}\,\overline{\kappa}\,\mathsf{of}\,\{(\overline{z_{i} : \STT_{i}}) : Q_i\} \big\}~\mathsf{else}~X 
%$$
%Intuitively, with the typeful update process we could explicitly define how to update a given location $l$, depending 
%on the current state of the protocols running in $l$. This update process can be as detailed as required: it allows to exhaustively specify how different states for the different sessions can lead to different adaptation routines $Q_k$. This brings extended precision to the specifications, also considering possible interleavings, as explained earlier when motivating a stop prefix for locations.
%
%It will be useful to have typeful update processes which are \emph{complete}; that is, 
%adaptation routines in the sense that, using session types, cover all possibilities for all involved sessions. One could also define a default option for typeful updates, to be carried out when none of the specified combinations of sessions actually matches.
%
%% \subsection{Some further issues}
%% Some further issues: 
%% \begin{itemize}
%% \item the typeful update should be defined in terms of variables...how/when the typeful update is instantiated with actual session channels? \\
%% idea: a two-step semantics for update. first, the location is stopped and the case is instantiated. second, the case is evaluated and the location is updated and restarted.
%% \item what if there is a mismatch between the number of open sessions in a given location, and the number of sessions that the update handles?
%% \end{itemize}

\section{Syntax and Semantics}\label{s:evadap}
ADD POINTERS TO TYPES
\subsection{Syntax}
In a nutshell, our session language is an integration of the synchronous $\pi$-calculus 
that we have considered in~\cite{DBLP:conf/sac/GiustoP13} with selected features from the eventful session framework introduced and studied in~\cite{Kouzapas12}.
Table~\ref{tab:syntax} reports the syntax of our language, together with the
relevant base sets: names, (session) channels, identifiers, expressions, and processes.

\begin{table}[t!]
$$
\begin{array}{lrlr}
u & ::=  &   x, y  \sepr a, b & \text{names}	\\
 k & ::=  &   x, y \sepr \cha^{+}, \cha^{-} & \text{channels}	\\
d & ::= & a, b  \,\sepr \cha^{+}, \cha^{-} & \text{identifiers} \\
v & ::= & \mathtt{true}, \mathtt{false} \sepr a, b  \sepr \cha^{+}, \cha^{-} & \text{values} \\
r	&::= &  \mathtt{upd}_I \sepr \mathtt{upd}_E \sepr\mathtt{upg} \sepr \cdots &\text{adaptation messages} \\
e & ::= & v \sepr x, y, z  \sepr d = d & \text{expressions} \vspace{0.5mm} \\
%  & \sepr & \arrive{u}  \sepr \arrive{k} \sepr \arrive{k,h} & \text{arrive predicates (usual)}\\ 
  & \sepr & \arrive{\locf{loc}, r} & \text{arrive predicate} \vspace{0.5mm}\\ 
P & ::=  &   \nopenr{u}{x:\ST}.P  & \text{session request}	\vspace{0.5mm} \\
	& \sepr &   \nopena{u}{x:\ST}.P  & \text{session acceptance}	\vspace{0.5mm} \\
	& \sepr &  \outC{k}{e}.P & \text{data output} \vspace{0.5mm}\\
  	&\sepr &    \inC{k}{x}.P  & \text{data input} \vspace{0.5mm} \\
	&\sepr&   \select{k}{n};P & \text{selection} \vspace{0.5mm}\\
    &\sepr&   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} & \text{branching} \vspace{0.5mm}\\
    &\sepr&   \mu \rv{X}.P & \text{recursion} \vspace{0.5mm} \\
	& \sepr &   \rv{X}& \text{recursion variable}  \vspace{0.5mm}\\
  	& \sepr &  \ifte{e}{P}{Q} & \text{conditional} \vspace{0.5mm}\\
  	& \sepr &   P \para  P & \text{parallel composition} \vspace{0.5mm}\\	 
		&\sepr&   \close{k}.P & \text{close session}	 \vspace{0.5mm}\\
	&\sepr&   \restr{\cha}{P}  & \text{channel hiding}	\vspace{0.5mm}\\
	&\sepr&   \restr{a}{P}  & \text{name hiding}	\vspace{0.5mm} \\
	&\sepr&   \mathbf{0}  & \text{inaction} \vspace{1.5mm} \\
	&\sepr&   \que{\cha}{\ST}  & \text{session queue} \vspace{0.5mm} \\ 
		&\sepr&  \scomponent{\locf{loc}}{P}  & \text{located process} \vspace{0.5mm} \\
%	&\sepr&  \nadapt{l}{P} & \text{update process}\\
	&\sepr&  \nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}} \quad& \text{typeful update process} \vspace{0.5mm}\\
	&\sepr&   \outC{\locf{loc}}{r}  & \text{adaptation signal} \vspace{0.5mm} \\
	&\sepr&   \que{\locf{loc}}{\til{r}}  & \text{queue for locations} 
%p	&::= &  + \sepr - &\text{channel polarities} \\
%h	&::= &  v \sepr n &\text{messages}  
%    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \mathtt{not}(e) \sepr  \ldots & \text{expressions}
\end{array} 
$$
\caption{Process syntax.} \label{tab:syntax}
\end{table}

TO DO: mention abbreviations (branching), notation for labels and locations, and close process, annotations for service requests,
location messages.

Our process language extends standard session $\pi$-calculi with 
\begin{enumerate}[(a)]
\item located processes; 
\item \emph{eventful update process}; 
\item runtime queues for session channels and locations; 
\item arrive predicate for locations.
\end{enumerate}
while located processes have been central in our previous works~\cite{DBLP:conf/sac/GiustoP13,BGPZFMOODS}, constructs (b)--(d) above have been first introduced in~\cite{Kouzapas12}. As 
we explain in detail next, here we adapt these constructs to the case of runtime adaptation (an issue not explored in~\cite{Kouzapas12}).

\emph{Located processes} are as in~\cite{DBLP:conf/sac/GiustoP13,BGPZFMOODS}: 
given a location \locf{loc}, 
process $\scomponent{\locf{loc}}{P}$ denotes a process $P$ which resides in $\locf{loc}$.
Locations are transparent: inside \locf{loc}, process $P$ can freely evolve, possibly interacting with its environment. 
Located process can be nested; this is particularly convenient when structuring process specifications for adaptability purposes.
\emph{Eventful update processes} are novel to this paper. They rely on the current state of the session protocols running within a given location in order to determine an appropriate adaptation operation. To better illustrate the intuitions behind this operator, we first discuss the particular case of \emph{diadic} eventful update processes; then we discuss the general $n$-adic case. 
A diadic eventful update process is written as follows:
\begin{equation}\label{eq:dya}
\nadaptbig{\locf{loc}}{\mycase{x_1, x_2}{{x_{1}^{}{:}\ST_{1}^{i} \,;\,  x_{2}^{}{:}\ST_{2}^{i}}}{Q_i}{i \in {I}}}
\end{equation}
The above process represents an adaptation routine for running sessions $\cha_1^p, \cha_2^q$ located  at $\locf{loc}$. 
Intuitively, this process works  as a case operator on the session protocols currently associated to channels $\cha_1^p, \cha_2^q$:
if such protocols match with one of the $\ST^j_1, \ST^j_2$ in the update process, then 
the current behavior at \locf{loc} will be replaced with the adaptation behavior $Q_j$.
Otherwise, if no such match is possible, then the current behavior at \locf{loc} is left unchanged and the update process at \locf{loc} is consumed. 
As formalized by the operational semantics (see below), an update process such as the one in \eqref{eq:dya} will be able to update at most two sessions established at \locf{loc}. This way, for instance, if the current behavior at \locf{loc} involves exactly one running session, and the update process offers an alternative $Q_j$ which requires only a single matching option, then runtime adaptation will be possible.

Eventful update processes represent both a generalization and a specialization of the $\mathtt{typecase}$ defined in~\cite{Kouzapas12}: they are a generalization, for $\mathtt{typecase}$ defines a case-like choice based only on the state of a single session; they are a specialization, for our generalized form of $\mathtt{typecase}$ is defined only for runtime adaptation purposes. In fact, while the $\mathtt{typecase}$ operator is defined in \cite{Kouzapas12} as part of the syntax of processes, here we limit its use to the case of update processes. This choice enables us to concentrate on identifying the key aspects of eventful session-based concurrency that are related to runtime adaptation. Also, the limited use of our generalized form of $\mathtt{typecase}$ is also useful to retain a standard session type syntax, as discussed in the following section. %simplify some parts of our technical development.

The general formulation for eventful update processes is given in Table~\ref{tab:syntax}. It 
generalizes the process in \eqref{eq:dya} by 
handling runtime adaptation for locations with at most $n$ running sessions:
\begin{equation}
\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}
\end{equation}
Notice that each option $i \in I$ may refer to a subset of the variables declared as $\til{x}$.

Eventful update processes are coupled with \emph{session queues}, which keep the current state of the session protocol at a given session channel. Hence, there is one queue for each open session. Session queues were first introduced in~\cite{Kouzapas12}, where they are also used as the intermediate medium that supports asynchronous session communication. Here we use session queues only to keep the session type that represents the current state of the session. Once again, this choice is align with our intention of identifying the minimal elements from the eventful session framework that are required to enhance runtime adaptation. An extension of the present framework to the asynchronous case is possible; see Remark X.

Here we also consider \emph{location queues}, not present in~\cite{Kouzapas12}, which are associated to locations and are key to handle adaptation requests.
In fact, location queues allow us to give an event-based, unified treatment to adaptation requests, both internal and external.
A queue for location \locf{loc} is a process denoted $\que{\locf{loc}}{\til{r}}$; messages $\til{r}$ are not related to communication as abstracted by session types. This  explicitly represents the fact that the issue and handling of adaptation requests and session exchanges are unrelated issues. Of course, runtime adaptation and communication are not unrelated phenomena: their relationship is meant to be mediated by the coupling of eventful update processes and the arrive predicate on locations, denoted \arrive{\locf{loc}, r}. %, which we now explain.
Inspired by the $\mathtt{arrive}$ predicate in~\cite{Kouzapas12}, this predicate intuitively checks if a certain message $r$ (which may represent a request for adaptation or upgrade) has been placed in the queue associated to some given location \locf{loc}. 

The arrive predicate \arrive{\locf{loc}, r} is useful to realize the overall vision of event-based runtime adaptation that we put forward in this paper. An adaptation request $r$ can be issued by a part of the specified system (an internal request) or by the environment interacting with the system (an external request). In either case, the request is formally issued by adding message $r$ to the queue associated to  location \locf{loc}, which encloses the behavior that should be adapted/modified. It is expected that associated eventful update processes do not occur freely in the process structure, but guarded within conditional constructs that enable adaptation depending on the arrival of some adaptation request. Hence, upon arrival of an adaptation request, such conditional constructs will release the previously guarded update processes, and adaptation may finally take place, depending on both the state of the protocols in the given location and the matching options specified by the update process. 

Summing up, this vision of runtime adaptation embodied by our language constructs enables us to formalize several concerns: using adaptation messages it formally explains \emph{who} may specify/trigger an adaptation event; by using queues  it also decrees \emph{how} an adaptation request is issued; by exploiting the arrive predicate we may also specify \emph{when} adaptation will be handled and triggered; by means of eventful update processes we may precisely specify \emph{what} is the goal of an adaptation event. 




\subsection{Semantics}
We now introduce the  reduction semantics for our process language.

The semantics relies on structural congruence TO BE ADDED.

It also relies on the following definitions of \emph{evaluation} and \emph{location} contexts:
\begin{eqnarray*}
\evc{E} & ::= & - \sepr \outC{k}{\evc{E}}.P \sepr  \ifte{\evc{E}}{P}{Q} \\
C,D & ::= & - \sepr \scomponent{\locf{loc}}{C \para P}
\end{eqnarray*}
Given 
$\locc{\!\!-\!\!}$
 (resp. $\evc{E}[-]$) we write $\locc{P}$ (resp. $\evc{E}[e]$) to denote 
the process (resp. expression) obtained by filling in the occurrences of hole $-$
in $C$ with $P$ (resp. in $\evc{E}$ with $e$).

\begin{table}[t!]
$$
\begin{array}{lc}
 \rulename{r:Open} & 
\locc{\nopena{u}{x:\ST}.P} \para  \locd{\nopenr{u}{y:\overline{\ST}}.Q} \pired \hfill  \\
& \hfill 
\restr{\cha}{\big({\locc{P\sub{\cha^+}{x} \para \que{\cha^p}{\ST}}  \para  \locd{Q\sub{\cha^-}{y} \para \que{\cha^{\overline{p}}}{\overline{\ST}} }\big) } \vspace{2.0mm} \\

\rulename{r:Com} &
\locc{\outCn{\overline{\cha}^{\,p}}{v}.P \para \que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\overline{\ST}}}} 
\pired \hfill \\
&\hfill
\locc{P \para \que{\cha^p}{\ST}} \para  \locd{Q\sub{{v}\,}{{x}} \para \que{\cha^{\overline{p}}}{\overline{\ST}} } %\quad ({e} \downarrow {c}) 
\vspace{2mm}
\\
%\rulename{r:Sel} &
%C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \para  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}} \} \para \\
%& D\{\select{\cha^{\,\overline{p}}}{n_j};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\overline{\ST_j} \}_{j \in J}}  \} 
%\pired \\
%& 
%\hfill C\{P_j \para \que{\cha^p}{\ST_j} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\overline{\ST_j}} \}  \quad (1 \leq j \leq m)  
\rulename{r:Sel} &
\locc{\branch{\cha^{\,p}}{n_j{:}P_j}_{j \in J} \para  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}}} \para 
\locd{\select{\cha^{\,\overline{p}}}{n_j};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\overline{\ST}_j \}_{j \in J}} } \\
& \pired \\
&  C\{P_j \para \que{\cha^p}{\ST_j} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\overline{\ST}_j} \}  \quad (j \in J)  
\vspace{2mm}
\\
\rulename{r:Clo} &
\locc{\close{\cha^{\,p}}.P \para \que{\cha^p}{\varepsilon} } \para  \locd{\close{\cha^{\,\overline{p}}}.Q \para \que{\cha^{\overline{p}}}{\varepsilon}} \pired %\\
%& \hfill 
\locc{P} \para  \locd{Q} \vspace{ 2mm}
\\
\rulename{r:Eva} & \text{if }e \pired e' \text{ then } \evc{E}[e] \pired \evc{E}[e']
\vspace{2mm}\\
 \rulename{r:Par} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{2mm}
\\
\rulename{r:Con} &  \text{if }P \pired P' \text{ then } \locc{P} \pired \locc{P'}
\vspace{2mm}\\
%  \rulename{r:Loc} &
% \text{if } P \pired P'~~\text{then}~~ \scomponent{l}{P} \pired \scomponent{l}{P'} \vspace{2mm}
% \\ 
\rulename{r:ResN} & \text{if }P \pired P' \text{ then } (\nu a)P \pired (\nu a)P'
\vspace{2mm}\\
\rulename{r:ResC} &\text{if }P \pired P' \text{ then } (\nu \cha)P \pired (\nu \cha)P'
\vspace{2mm}\\
 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{2mm}
\\
 \rulename{r:Rec} &
\recu\,\rv X. P \pired P\subst{\recu\,\rv X. P }{\rv X}
\vspace{2mm}\\
\rulename{r:IfTr} &
\ifte{\mathtt{true}}{P}{Q} \pired P    \vspace{2mm}
\\
 \rulename{r:IfFa} &
\ifte{\mathtt{false}}{P}{Q} \pired Q   \vspace{2mm}\\
\rulename{r:UReq} &  \locc{\que{\locf{loc}}{\til{r}_1}} \para \locd{\outC{\locf{loc}}{r}} \pired 
\locc{\que{\locf{loc}}{\til{r}_1 \cdot r}} \para \locd{\mathbf{0}}
\vspace{2mm}\\
\rulename{r:Arr} & \locc{\evc{E}[\arrive{\locf{loc},r}]} \para \locd{\que{\locf{loc}}{\til{r}}} \pired \locc{\evc{E}[\mathtt{b}]}
\para \locd{\que{\locf{loc}}{\til{r}}}  \quad ((|\til{r}| \geq 1) \downarrow \mathtt{b}) 
\vspace{4mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{r:Upd} & 
\displaystyle\frac{
\begin{array}{rcl} 
\mathsf{fc}(P) = \til{\cha} = \cha_1^p, \ldots, \cha^p_n 
& &
R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} \\
 (V = P \land R' = R) & \bigvee  &
\exists \til{x}_0 \subseteq \til{x}, \rho .\big(
|\til{k}| = |\til{x}_0| \land \til{x}_0 = \{x_1, \ldots, x_g\} ~\land ~
\\ 
& & \qquad \rho = \subst{\til{\cha}\,}{\,\til{x}_0} ~\land~ I' = \{u \in I \,|\, \mathsf{fc}(Q_u) = \til{x}_0\}~\land\\
& & \qquad \exists l \in I'.(\forall j \in [1..n].\forall s \in [1..g].~~ \STT^{l}_s \leq \ST_j ~\land~ \\
&& \qquad 
\forall r < l.\exists j \in [1..n].\exists s \in [1..g].~~\STT^{r}_s \not\leq \ST_j ~\land~
\\
&&  \qquad V = \rho(Q_l) ~\land~
R' = \que{\cha^p_1}{\STT_{1}^l} \para \cdots \para \que{\cha^p_n}{\STT^{l}_g} 
)  \big)
\end{array}
}{
\begin{array}{l}
\locc{\scomponent{\locf{loc}}{P \para R}} \para
\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}}   
\pired \qquad \\
\hfill \locc{\scomponent{\locf{loc}}{V \para R'}} \para \locd{\mathbf{0}}
\end{array}
} 
\vspace{4mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\rulename{r:Upd2} & 
%\displaystyle\frac{
%\begin{array}{c} 
%\mathsf{fc}(P) = \til{\cha} = \cha_1^p, \ldots, \cha^p_n \qquad
%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} \\
% (V = P \land R' = R)  ~~\bigvee~~  \\
%\exists \til{x}_0 \subseteq \til{x}, \rho .\big(
%|\til{k}| = |\til{x}_0| \land \til{x}_0 = \{x_1, \ldots, x_g\}  ~\land~ I' = \{u \in I \,|\, \mathsf{fc}(Q_u) = \til{x}_0\}~\land\\
% \exists l \in I'.(\forall j \in [1..n].\forall s \in [1..g].~~ \STT^{l}_s \leq \ST_j ~\land~  
%\forall r < l.\exists j \in [1..n].\exists s \in [1..g].~~\STT^{r}_s \not\leq \ST_j ~\land~ \\
%  \quad  
%\rho = \subst{\til{\cha}\,}{\,\til{x}_0} ~\land ~ V = \rho(Q_l) ~\land~
%R' = \que{\cha^p_1}{\STT_{1}^l} \para \cdots \para \que{\cha^p_n}{\STT^{l}_g} 
%)  \big)
%\end{array}
%}{
%\begin{array}{l}
%\locc{\scomponent{\locf{loc}}{P} \para R} \para
%\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}}   
%\pired \qquad \\
%\hfill \locc{\scomponent{\locf{loc}}{V} \para R'} \para \locd{\mathbf{0}}
%\end{array}
%} 
\end{array}
$$
\caption{Reduction Semantics\label{tab:redsem}}
\end{table}



The rules of the semantics are given in Table~\ref{tab:redsem}. The first four rules formalize session behavior within hierarchies of nested locations. In rule~\rulename{r:Open} the synchronization on a channel $u$ with dual behaviors leads to the establishment of a
fresh session, which in our case entails also the creation of a session queue with the prescribed behavior.
Rule~\rulename{r:Com} represents session communication of a value: following~\cite{Kouzapas12}, in addition to requiring complementary session prefixes, we also require that the type contained in the respective session queue supports an input and output behavior. After the reduction, both prefixes in the process and prefixes in the session types are consumed. Rule~\rulename{r:Sel} for intra-session selection is standard, augmented with queue information. Rule~\rulename{r:Clo} formalizes coordinated session termination. It is worth observing that we require that session queues are \emph{local} to the process. This way, for instance, a process 
\begin{equation}
\locc{\outCn{\overline{\cha}^{\,p}}{v}.P} \para \loccp{\que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\overline{\ST}}} \nonumber
\end{equation}
is not able to reduce for the queue $ \cha^p$ is not local to the process executing that session.
The following nine rules in the table are standard and/or self-explanatory: they define, respectively, reduction under evaluation contexts, parallel composition, located context, and restriction; applications of structural congruence; recursion and conditional operators.

The last three rules define the eventful approach to runtime adaptation. Rule~\rulename{r:UReq} assimilates the issue of an adaptation request to a synchronization between a queue and an adaptation message. Notice that we explicitly allow requests to be added remotely, i.e., the queue and the message may be in different location contexts. Rule~\rulename{r:Arr} resolves arrive predicates within evaluation contexts; it requires to query the current content of the queue, which may be remotely located. Rule~\rulename{r:Upd} gives semantics to eventful update process. While at a first sight it may appear complex, it actually enforces a very simple case operation over the running sessions at location \locf{loc}. The rule attempts to match (via subtyping, see next section) the current protocol state at \locf{loc} (embodied by the open sessions $\til{\cha}$ and their associated queues $R$) with the different options offered by the update process. The rule focuses on the first positive match that holds. If no such 
match exists then the current behavior at the location (represented by $P$) is left unchanged, and the update operation is consumed. 





\subsection{An Example}

We consider a simple scenario in which a server and a client communicate to achieve a given goal. 
We will illustrate the following distinctive aspects of our framework:
\begin{enumerate}[$-$]
\item The use of typeful update processes to enforce runtime adaptation that depends on the state of the running sessions
\item The use of adaptation requests inside processes to invoke adaptation routines
\item How to handle external adaptation requests
\end{enumerate}

Consider the following processes. We have a single-instance service (on name $u$) and a corresponding client; they reside in 
different 
locations, denoted  \locf{ser} and \locf{cli}, respectively. 
The server is associated to a manager $M_\locf{ser}$ which should spawn an adaptation routine %$A_\locf{ser}$ 
in two cases:
\begin{enumerate}[(1)]
\item A known component of the system (the client or the server itself) issues an adaptation request for service $u$
\item A non specified part of the system (say, its surrounding environment) issues an adaptation request
\end{enumerate}
We may formalize this scenario as follows:
\begin{eqnarray*}
Sys & =  & \scomponentbig{\locf{ser}}{ \nopena{u}{x{:}\ST}.\branchbig{x}{ l_1{:}Q_x \alte l_2{:}\branch{x}{n_1{:}P_x^1 \alte n_2{:}P_x^2}} \para M_\locf{ser}} \para \\
%& = & ~\scomponentbig{\locf{cli}}{ \nopenr{u}{y:\ST}.(\outC{\locf{ser}}{\mathtt{upd}_I} \para \select{y}{l_2};\select{y}{n_2};R'_y) } \\
&   & ~\scomponentbig{\locf{cli}}{ \nopenr{u}{y{:}\overline{\ST}}.R_y } \\
M_\locf{ser} & =  & \que{\locf{ser}}{\epsilon} \para \mu \rv{X}.\ifte{\arrive{\locf{ser}, \mathtt{upd}_I}}{A_\locf{ser}}{\rv{X}}
 \\
& & \qquad  ~~\para \mu \rv{X}.\ifte{\arrive{\locf{ser}, \mathtt{upd}_E}}{B_\locf{ser}}{\rv{X}}
\end{eqnarray*}
where we assume $\ST = \&\{l_1{:}\alpha_1\,,\,   l_2{:}\&\{n_1{:}\alpha_{21} \,,\,  n_2{:}\alpha_{22} \}\}$.
Thus, the service on name $u$ offers two main options to the client, which are distinguished with labels $l_1$ and $l_2$.
In case that the second option is selected, a further choice becomes available with labels $n_1$ and $n_2$. Notice that 
all of these possibilities entail different behaviors (denoted $Q_x$, $P_x^1$, and $P_x^2$, respectively). 
Observe also that   $M_\locf{ser}$ includes three components (a)~the queue for adaptation requests (internal or external) for the service
at \locf{ser}; (b)~a process ready to react if an internal adaptation request does arrive;
and (c)~a process ready to react to an external adaptation request. 

Suppose now that client and 
service interact on $u$ to establish the session. 
Assume further that the client's body $R_y$ includes, in addition 
to their communication behavior, 
 the issue of an adaptation request 
for the service. 
This is a natural possibility for clients, for they would like to interact with the latest available version of the service:
$$
R_y = \outC{\locf{ser}}{\mathtt{upd}_I} \para \select{y}{l_2};\select{y}{n_2};R'_y
$$
Hence, after the synchronization on $u$ we obtain:
\begin{eqnarray*}
Sys & \pired  & \scomponentbig{\locf{ser}}{\branchbig{\cha^+}{ l_1{:}Q_{\cha^+} \alte l_2{:}\branch{\cha^+}{n_1{:}P_{\cha^+}^1 \alte n_2{:}P_{\cha^+}^2}} \para M_\locf{ser}} \para \\
&   & ~\scomponentbig{\locf{cli}}{\outC{\locf{ser}}{\mathtt{upd}_I} \para \select{\cha^-}{l_2};\select{\cha^{-}}{n_2};R'_{\cha^{-}} } = Sys_1
\end{eqnarray*}
In a purely asynchronous setting, in which we further assume explicitly distributed resources and services, it is unrealistic to attempt at predicting when the adaptation request issued by the client will be actually served. This brings us to the question: when the request is finally handled, what should be the appropriate adaptation routine for the endpoint $\cha^+$? That is, what should be the actual structure of process $A_\locf{ser}$? Let us assume the following possibilities:
\begin{enumerate}[(a)]
\item If the first branching has not been  decided yet (the actual session has not yet started), then add an extra service $l_3{:}Q'$.
\item If both labels $l_2$ and $n_1$ have been selected by the client, then offer an new behavior that replaces $P_{\cha^+}^1$.
Proceed similarly if both $l_2$ and $n_2$ have been selected.
\item Otherwise, if  none of the above options apply then  keep the service as it is.
\end{enumerate}
These three possibilities represent a style of specification for adaptation routines that refers to concrete states within the structure of the session. As such, it goes beyond the routines expressible in previous works. We now illustrate how an appropriate adaptation routine that captures (a)--(c) can be expressed in our framework. We have the following process for $A_\locf{ser}$:
\begin{eqnarray*}
A_\locf{ser}  =  \nadaptbig{\locf{ser}}{\mathsf{case}\,x\,\mathsf{of}\{(x{:}\ST):P^* ~\alte~ (x{:}\ST_{21}):P^3_{x}  ~\alte~ (x{:}\ST_{22}):P^4_{x} \, \}} 
\end{eqnarray*}
where 
$P_x^3$ (resp. $P_x^4$) is an alternative implementation for $P_x^1$ (resp. $P_x^2$), and $P^*$ stands for 
the following extended service definition:
\begin{eqnarray*}
\branchbig{x}{ l_1{:}Q_x \alte l_2{:}\branch{x}{n_1{:}P_x^1 ~\alte n_2{:}P_x^2} \alte l_3{:}Q'_x}
\end{eqnarray*}
With this definition for $A_\locf{ser}$, adaptation can be enforced independently of the actual moment in which 
the internal adaptation request is issued and detected by $M_\locf{ser}$.

Observe that the adaptation routine specified by the typeful update process in $A_\locf{ser}$
specifies the cases in which a concrete behavior modification is meant to occur at runtime. 
This is enough, for the semantics that we have presented 
formalizes a ``default'' adaptation: 
if none of the specified cases holds, then the current state of the session will be preserved in location $\locf{ser}$.
Also, it is worth stressing that the update process in $A_\locf{ser}$ corresponds to the simple case in which only one session needs to be taken into account. Our typeful adaptable processes can handle an arbitrary (but finite) number of sessions. This could come in handy when considering, for instance, a location with several different clients for the same service. 

Finally, it is interesting to notice that the treatment of external adaptation requests are treated analogously. 
Observe that location identities (such as \locf{ser} or \locf{cli}) are public, and so the
queues that we use to trigger adaptation events could be visible to the external environment.
This brings uniformity to specifications, and allows us to consider open systems for adaptation purposes.



\section{Types}
 In this section we briefly introduce our typing system. Type syntax follows standard notation \cite{DBLP:journals/entcs/YoshidaV07} and extends the one in \cite{DBLP:conf/sac/GiustoP13}.

 
\begin{definition}[Types]\label{d:types}
The syntax of 
 \emph{basic types} (ranged over $\capab, \sigma,   \ldots$) 
and 
 \emph{session types} (ranged over $\ST, \beta, \ldots$)
is:
$$
\begin{array}{lclr}
T&::=& \capab, \alpha \\
\capab, \sigma & ::= & \mathsf{name} \sepr \mathsf{bool}  ~~~& \text{basic types}\\

\alpha, \beta &::=  &  !(\capab).\alpha \sepr ?(\capab).\alpha & \text{send, receive} \vspace{0.5mm}\\ 
		& \sepr &  !(\beta).\alpha \sepr ?(\beta).\alpha & \text{throw, catch}  \vspace{0.5mm}\\ 
		& \sepr &  \&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}  \quad &  \text{branch} \vspace{0.5mm} \\
		& \sepr &  \oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}  &  \text{select} \vspace{0.5mm} \\
		& \sepr &  \epsilon \!\!\!\!\!\!& \text{closed session} \vspace{0.5mm} \\
    & \sepr  & t & \text{type variable} \vspace{0.5mm} \\ 
   	      & \sepr &  \mu t.\alpha & \text{recursive type} 
\end{array}
$$

\end{definition}

We recall the intuitive meaning of session types. 
We write $\til{\tau}$ to denote a sequence of base types $\tau_1, \ldots, \tau_n$.
Type $?(\til{\capab}).\ST$ (resp. $?(\beta).\ST$) abstracts the behavior of a channel 
which receives values of types $\til{\capab}$ (resp. a channel of type $\beta$) 
and continues as $\ST$ afterwards.
Complementarily, type $!(\til{\capab}).\ST$ (resp. $!(\beta).\ST$) represents the behavior
of a channel which sends values (resp. a channel)  and that continues as $\ST$ afterwards.
Type $\&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}$ describes a branching behavior, or external choice, along a channel:
it offers $m$ behaviors, and if the $j$-th alternative is selected then it behaves as described by type $\ST_j$ ($1 \leq j \leq m$).
In turn, type $\oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}$ describes the behavior of a channel which 
may select a single behavior among  $\alpha_1, \ldots, \alpha_m$. This is an internal choice, which continues as $\ST_j$ afterwards.
Finally, type $\epsilon$ represents a channel with no communication behavior. 

Next we introduce the subtyping relation.


\begin{definition}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{type simulation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\capab \bsub \sigma$.

\item If $\unf{\ty} = \epsilon$ then $\unf{\tyy} = \epsilon$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = ?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\ty_2, \tyy_2)  \in \mcc{R}$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,!(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\tyy_2, \ty_2)  \in \mcc{R}$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\tau_i, \sigma_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = !(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\sigma_i, \tau_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = \&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
and $m \leq h$
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
and $h \leq m$
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}
\end{definition}

%Observe how  $\subt$ is co-variant for input prefixes and contra-variant for outputs, 
%whereas it is co-variant for branching and contra-variant for choices.
We have the following definition:


\begin{definition}
The coinductive subtyping relation, denoted \csub, is defined by $T \csub S$ if and only if there exists a type simulation $\mcc{R}$
such that $(T, S) \in \mcc{R}$.
\end{definition}

In a similar way to subtyping duality is defined coinductively:


\begin{definition}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{duality relation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\tau \csub \sigma$ and  $\sigma \csub  \tau$.

\item If $\unf{\ty} = \epsilon$ then $\unf{\tyy} = \epsilon$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = !(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = \&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1, \dots,  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1, \dots,  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}

\end{definition}

We may now define:

\begin{definition}
The coinductive duality relation, denoted \cdual, is defined by $T \cdual S$ if and only if there exists a duality relation $\mcc{R}$
such that $(T, S) \in \mcc{R}$. The extension of $\csub$ to typings and interfaces, written $\ActS \csub \ActS'$ and $\INT \csub \INT'$, respectively, 
arise as expected.
\end{definition}


Our typing judgments generalize usual notions with an  \emph{interface}~$\INT$ (see Def.~\ref{d:interf}). 
Based on the syntactic occurrences of prefixes $\nopenr{a}{x:\ST}$, and $\nopena{a}{x:\ST}$,
the interface of a process describes the (possibly persistent) services appearing in it.
Thus, intuitively, the interface of a process gives an ``upper bound'' on the services that a process may execute.
Formally, we have:


\begin{definition}[Interfaces]\label{d:interf}
We define an \emph{interface} as the multiset whose underlying set of elements 
$\mathrm{Int}$ contains 
assignments from names to session types which are qualified (cf. Table~\ref{tab:types}).
More precisely: $$\mathrm{Int} = \{ \qua\,a{:}\ST ~|~ \qua \in \{\qual, \quau\}, 
\text{$a$ is a name, and $\ST$ is a session type}\}$$
We use $\INT, \INT', \ldots$ to range over interfaces.
We sometimes write $\#_\INT(a) = h$ to mean that element $a$ occurs $h$ times in $\INT$.
\end{definition}

Observe how several occurrences of the same service declaration are captured by the multiset nature of interfaces.
The union of two interfaces $\INT_1$ and $\INT_2$ is essentially the union of their underlying multisets.
We sometimes write $\INT \addelta a:\ST_\qual$ 
and  $\INT \addelta a:\ST_\quau$
to stand 
for $\INT \addelta\{\qual\,a{:}\ST\}$ and 
$\INT \addelta \{\quau\,a{:}\ST\}$, respectively.

\begin{newnotation}[Interfaces]\label{n:interf}
We write $\INT_\qual$ (resp. $\INT_\quau$) to denote the subset of $\INT$ involving
only assignments qualified with $\qual$ (resp. $\quau$). 
Moreover, we write $\INT \unres$ to denote the ``persistent promotion'' of $\INT$. Formally, 
$\INT \unres = \INT \setminus \INT_\qual \addelta \{\quau\,a{:}\ST \mid   \qual\,a{:}\ST \in \INT_\qual \}$.
\end{newnotation}

It is useful to relate different interfaces. 
This is the intention of the relation $\intpr$ over interfaces, defined next.

\begin{definition}[ Interface Preorder] \label{d:rintpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr \INT'$ iff 
\begin{enumerate}[1.]
\item $\forall (\qual\,a{:}\ST)$ such that  
 $\#_{\INT_\qual}(\qual\,a{:}\ST) = h$  with $h > 0$,
then  one of the following holds:
\begin{enumerate}[(a)]
\item there exists $h$ distinct elements $(\qual\,a{:}\STT_i) \in \INT'_\qual$ such that 
 $\ST \csub \STT_i$ for $ i \in [1..h]$;
\item there exists $(\quau\,a{:}\STT) \in \INT'_\quau$ such that  $\ST \csub \STT$.
\end{enumerate}
\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then $ (\quau \, a{:}\STT) \in \INT'_\quau $ and $\ST \csub \STT$, for some $\STT$.
\end{enumerate}


\end{definition}


%\subsection{Environments, Judgments and Typing Rules}
\begin{table}[t!]
\textsc{Environments}
$$
\begin{array}{lclr}
		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  k:\que{}{\ST}  & \text{typing with active sessions} \vspace{0.5mm} \\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST}_\qua \rangle \quad& \text{first-order environment} \vspace{0.5mm} \\
\Theta &::= &  \emptyset \sepr  \Theta,\rv{X}:\type{\ActS}{\INT} \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
\end{array}
$$  
\caption{Types and Typing Environments. Interfaces $\INT$ are formally introduced in Definition~\ref{d:interf}.}\label{tab:types}
\end{table}
% 


The typing environments we rely on are defined in Table~\ref{tab:types}.
In addition to interfaces $\INT$, we consider typings $\ActS$ and environments $\Gamma$ and $\Theta$. 
Typing $\ActS$ is commonly used to collect
assignments from channels to session types; as such, it describes
currently active sessions. 
In our discipline, 
in $\ActS$ we also include \emph{bracketed assignments}, denoted $\kappa^p:\que{}{\ST}$,
which represent the type for queues. 
We write $dom(\ActS)$ to denote the set $\{ k^p \mid k^p:\ST \in \ActS \lor [k^p:\ST] \in \ActS\}$.
We write $\ActS , k:\ST $  where $k \not\in dom(\ActS)$.


$\Gamma$ is a first-order environment which maps expressions to basic types
and names to pairs of \emph{qualified} session types.
In  the interface, a session type is qualified with 
`$\quau$' if it is associated to a persistent service; otherwise, it is qualified with 
`$\qual$'.

The higher-order environment $\Theta$ 
collects assignments of process variables and locations to interfaces. 
While the former kind of assignments is relevant to recursive processes, the latter concern located processes.
As we explain next, by relying on the combination of these two pieces of information the type system ensures that
runtime adaptation actions preserve the behavioral interfaces of a process.
We write $vdom(\Theta)= \{ \mathsf{X} \mid \mathsf{X}:\INT \in \Theta \}$ to denote the variables in the domain of $\Theta$.
Given these environments, a \emph{type judgment} is  of form
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $$ 
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface 
$\INT$.

\begin{definition}%[Well-typed process]
A process is well-typed if it can be typed using the rules in Tables~\ref{tab:ts} and~\ref{tab:session}.
\end{definition}


\begin{table}[th!]
$$
\begin{array}{c}

\inferrule*[right=\rulename{t:LocEnv}]{ }{\typing{\Theta, \locf{loc}:\INT}{\locf{loc}}{\INT}} 
\quad \infer[\rulename{t:Que}]
 {\judgebis{\env{\Gamma}{\Theta}}{\que{\cha}{\ST}}{\type{\cha:\que{}{\ST}}{\emptyset}}}{}
\vspace{2mm} \\

\infer[\rulename{t:msg}]
{\typing{\Gamma}{r_1}{\msg}}{} \qquad

\infer[\rulename{t:locQ}]
{\typing{\Gamma}{r_1;\til{r}}{\msg}}
{\typing{\Gamma}{\til{r}}{\msg} & \typing{\Gamma}{r_1}{\msg}}\vspace{2mm} \\

\infer[\rulename{t:arrive}]
{\judgebis{\env{\Gamma}{\Theta}}{\arrive{\locf{loc}, r}}{\bool}}
{\typing{\Theta}{\locf{loc}}{\INT} \qquad\typing{\Gamma}{r}{\msg}} \vspace{2mm} \\


\inferrule*[right=\rulename{t:Loc} ]
 {
       \typing{\Theta}{\locf{loc}}{\INT} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } }  \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{\locf{loc}}{}{\INT}{P} }{ \type{\ActS}{\INT' }}}
\vspace{2mm} \\

\infer[\rulename{t:Sig}]
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\locf{loc}}{r}}{\type{\emptyset}{\emptyset}}}
{\typing{\Gamma}{r}{\msg}} \qquad

\infer[\rulename{t:QLoc}]
{\judgebis{\env{\Gamma}{\Theta}}{\que{\locf{loc}}{\til{r}}}{\type{\emptyset}{\emptyset}}}
{ \typing{\Gamma}{\til{r}}{\msg}} \vspace{2mm} \\


\infer[\rulename{t:Adapt}]
{\judgebis{\env{\Gamma}{\Theta}}{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{j}; \cdots ;x_{m_j}^{}{:}\STT_{m_j}^{j}}}{Q_j}{j \in J}}}{\type{\emptyset}{\emptyset}}}
{\typing{\Theta}{\locf{loc}}{\INT} & \forall j \in J, \ 
\judgebis{\env{\Gamma}{\Theta}}{Q_i}{\type{x_{1}^{}{:}\STT_{1}^{j}; \cdots ;x_{m_j}^{}{:}\STT_{m_j}^{j}}{\INT_j} } \quad \INT_j \intpr \INT}

\vspace{2mm} \\
\infer[\rulename{t:RVar}]{\Gamma; \Theta,\rv X: \ActS, \INT \vdash \rv X:\type{\ActS}{\INT}}{}
\quad
\infer[\rulename{t:Rec} ]{\judgebis{\env{\Gamma}{\Theta}}{\mu \rv X. P}{\type{\Delta}{\INT }}} 
{\judgebis{\env{\Gamma}{\Theta,\rv X: \type{\ActS}{\INT}}}{P}{\type{\Delta}{ \INT}} }
\vspace{2mm} \\
\infer[\rulename{t:Subs} ]{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS'}{\INT'}} } 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{ \INT}}& \ActS \csub \ActS' & \INT \intpr \INT'}
\vspace{2mm} \\
 
 \infer[\rulename{t:CRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST_1, \cha^-:\que{}{\ST_1}, \cha^+:\ST_2, \cha^+:\que{}{\ST_2} }{ \INT}} & \ST_1 \cdual \ST_2} \vspace{2mm} \\
 
 \infer[\rulename{t:NRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{a}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS }{ \INT \cup \INT_a}} \quad  \ a \notin \dom{\INT} }\\
 \text{ where } \INT_a \text{ contains only declarations for } a \ (i.e. \forall b\neq a, b\notin \dom{\INT_a} )
 
\end{array}
 $$
\caption{Well-typed processes (I)} \label{tab:ts}
\end{table}





\begin{table}[th!]
DA SPOSTARE IN APPENDICE
$$
\begin{array}{c}
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\infer[\rulename{t:bool}]
{\typing{\Gamma}{\true, \false}{\bool}}{} 
\qquad
\infer[\rulename{t:name}]
{\typing{\Gamma}{a}{\name}}{} 
\vspace{2mm} \\
\infer[\rulename{t:bVar}]
{\typing{\Gamma, x: \bool }{x}{\bool}}{} 
\qquad
\infer[\rulename{t:nVar}]
{\typing{\Gamma, x: \name}{x}{\name}}{} 
\vspace{2mm} \\
\infer[\rulename{t:eq}]
{\typing{\Gamma}{d=d}{\bool}}{} \qquad 
\infer[\rulename{t:Ser}]
{\typing{\Gamma, u:\langle\ST_\qua, \overline{\ST}_\qua\rangle}{u}{\langle\ST_\qua, \overline{\ST}_\qua\rangle}}{} 
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Nil}]{ }{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Accept}]
{\typing{\Gamma}{u}{\langle \ST_\qual , \overline{\ST}_\qual  \rangle} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST}{\,\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\nopena{u}{x:\ST}.P}{ \type{\ActS}{\,\INT \addelta u: \ST_\qual}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Request}]
 {\typing{\Gamma}{u}{\langle \ST_\qua , \overline{\ST}_\qual \rangle} \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST }{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{ \nopenr{u}{x:\ST}.P}{ \type{\ActS}{\,\INT \addelta u: {\ST}_\qual }}} 
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Clo}]
 {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \quad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}}
\quad
\inferrule*[right=\rulename{t:Par}]
 {
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \quad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}

\vspace{2mm} \\
\inferrule*[right=\rulename{t:Thr}] 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}}
\quad
\inferrule*[right=\rulename{t:Cat}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:In}]
{\judgebis{\env{\Gamma, {x}:{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{{x}}.P }{\type{\ActS, k:?({\capab}).\ST}{ \INT}}}
\quad 
\inferrule*[right=\rulename{t:Out}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \quad \typing{\Gamma}{e}{\capab}}
{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{{e}}.P}{\type{\ActS, k:!({\capab}).\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Weakc}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \quad \cha^+, \cha^- \notin dom(\ActS)}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT }}}
 
\quad
\inferrule*[right=\rulename{t:Weakn}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \quad a \notin dom(\INT)}
{\judgebis{\env{\Gamma}{\Theta}} {\restr{a}{P}}{\type{\ActS}{ \INT }}}


\vspace{2mm} \\
\inferrule*[right=\rulename{t:If}]
 {
 \typing{\env{\Gamma}{\Theta}}{ e}{\mathsf{bool}} \ 
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \ 
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
 }{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} 
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Bra}] 
{
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS, k:\ST_1}{ \INT_1}} 
\quad 
\cdots
\quad
\judgebis{\env{\Gamma}{\Theta}}{P_m}{\type{\ActS, k:\ST_m}{ \INT_m}} \quad \INT = \INT_1 \uplus ...\uplus \INT_m
 }{\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1{:}P_1 \alte \cdots \alte  n_m{:}P_m}}{\type{ \ActS, k:\&\{n_1{:}\ST_1, \ldots, n_m{:}\ST_m \}}{\INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Sel}]
{
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST_i}{ \INT}} \qquad 1 \leq i \leq m 
}{\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i};P}{\type{\ActS, k:\oplus\{n_1:\ST_1, \ldots,  n_m:\ST_m \}}{\INT}}}
\end{array}
$$% \vspace{-4mm}
\caption{Well-typed processes (II)}\label{tab:session}
\end{table}

We comment on some  of the rules in Table~\ref{tab:ts}, other rules are standard and self explanatory.
Rule \rulename{t:Adapt} types update processes. Notice that the typing rule ensures each process $Q_i$ has exactly the same active sessions that those declare in the respective case.   The requirement $\INT_j \intpr \INT$ guarantees that the process behavior does not ``exceed'' the expected behavior within the location.
Rule  \rulename{t:Subs}  takes care of  subtyping both for typings $\ActS$ and interfaces. Finally rule~\rulename{t:CRes} types channel restriction that ensures typing duality among partners of a session and their respective queues.
Typing of queues is given by rule \rulename{t:Que} that simply assigns to queue $\que{\kappa}{\ST}$ type $\kappa:\que{}{\ST}$.
Finally rule \rulename{t:NRes} types hiding of services names, by simply removing their declarations from the interface $\INT$ of the process.
% restricted end-points are not removed from $\ActS$ but kept in bracketed form, as motivated earlier. 
% Using typing $\ActS$,
% we can have an exact count of open, possibly restricted, sessions in a process.
% Rule~\rulename{t:Close} types the explicit session closure construct, extending 
% $\ActS$ with a fresh channel which is assigned to an empty session type. 
% This may be useful to understand why our typing rule for the inactive process (rule \rulename{t:Nil})
% requires an empty typing $\Delta$.
% 
% %\jp{Far notare la nostra regola Rule \rulename{t:Nil} inizia da un $\Delta$ vuoto...}
% Rule~\rulename{t:Loc} performs two checks to type located processes. First, the runtime annotation 
% $h$ is computed by counting the assignments (standard and bracketed) declared in $\ActS$ (see~\ref{ap:count}). 
% Second, the rule checks that the interface of the located process is less  or equal (in the sense of $\intpr$, cf. Not.~\ref{n:interf}) than the
% declared interface of the given location. 
% Informally, this ensures that the process behavior does not ``exceed'' the expected behavior within the location.
% It is worth observing how a typed located processes has the exact same typing and interface of its contained process:
% this is how transparency of locations arises in typing.
% Finally, rule \rulename{t:Adapt} types update processes. Observe how the interface associated to the process variable of the given 
%  adaptation routine should match with the declared interfaces for the given location. 
% However, for simplicity we establish no condition on the relation between $\INT$ (the expected interface) 
% and $\INT'$ (the interface of the adaptation routine $P(\mathsf{X})$)
% %---Sect.~\ref{sec:int} 

The type system we have introduced enjoys subject reduction, the proof is rather standard.

\begin{theorem}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT'}}$, for some $\INT'$.
\end{theorem}
\begin{proof}
The proof proceeds by induction on the last rule applied in the reduction. %See~\ref{app:subred} for details. 
We sketch the case of \rulename{r:Upd}, other cases are standard and therefore omitted.
For simplicity and without loss of generality we omit contexts $C$ and $D$.
\newcommand{\jug}{\ensuremath{\mathcal{S}}}



From Table~\ref{tab:redsem} we have:
$$
\begin{array}{l}
{\scomponent{\locf{loc}}{P \para R}} \para
{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}}   
\pired \qquad \\
\hfill {\scomponent{\locf{loc}}{V \para R'}} \para {\mathbf{0}}
\end{array}
$$
with $R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n}$.

By assumption we have 
$$\judgebis{\env{\Gamma}{\Theta}}{{\scomponent{\locf{loc}}{P} \para R} \para
{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}}   
}{ \type{\ActS}{\INT}}$$
Then, by inversion on typing using rules \rulename{t:Par}, \rulename{t:Adapt}, and \rulename{t:Loc} we infer:
\begin{equation}\label{eq:srupd00}
\infer
{\judgebis{\env{\Gamma}{\Theta}}{{\scomponent{\locf{loc}}{P \para R}} \para
{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}}   
}{ \type{\ActS}{\INT}}}
{
\eqref{eq:srupd0}
&
\eqref{eq:srupd1}
}
\end{equation}
Subtree \eqref{eq:srupd0}  and \eqref{eq:srupd1} are as follows:
\begin{equation}\label{eq:srupd0}
\infer{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{\locf{loc}}{P \para R} }{ \type{\ActS}{\INT}}}
{ \INT \intpr \INT^* & \typing{\Theta}{\locf{loc}}{\INT^*}
  & \judgebis{\env{\Gamma}{\Theta}}{P \para R}{\type{\ActS}{\INT} }   }
\end{equation}
\begin{equation}\label{eq:srupd1}
\infer{\judgebis{\env{\Gamma}{\Theta}}{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}}{\type{\emptyset}{\emptyset}}}
{\typing{\Theta}{\locf{loc}}{\INT^*} & \forall j \in J, \ 
\judgebis{\env{\Gamma}{\Theta}}{Q_i}{\type{x_{1}^{}{:}\STT_{1}^{j}; \cdots ;x_{m_j}^{}{:}\STT_{m_j}^{j}}{\INT_j} } \quad \INT_j \intpr \INT^*}
\end{equation}
Now, we can reconstruct the type derivation for  process ${\scomponent{\locf{loc}}{V \para R'}} \para {\mathbf{0}}$ after the reduction. 
We have two cases, either the typeful update has not been applied or it is. In the first case the theorem is immediately satisfied with $\INT' = \INT$. In the second case $V = \rho(Q_l)$ and $
R' = \que{\cha^p_1}{\STT_{1}^l} \para \cdots \para \que{\cha^p_n}{\STT^{l}_g}$ and we obtain the following derivation tree using rules \rulename{t:Par} and \rulename{t:Subs}:
\begin{equation}\label{eq:finupd}
\infer{\judgebis{\env{\Gamma}{\Theta}}{{\scomponent{\locf{loc}}{V \para R'}} \para {\mathbf{0}}}{ \type{\ActS}{\INT_l}}}
{\infer
{\judgebis{\env{\Gamma}{\Theta}}{{\scomponent{\locf{loc}}{V \para R'}} \para {\mathbf{0}}}{ \type{\ActS'}{\INT_l}}}
{ \judgebis{\env{\Gamma}{\Theta}}{{\scomponent{\locf{loc}}{V \para R'}} }{ \type{\ActS'}{\INT_l}}
 & \judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset} }}
 & \ActS' \csub \ActS & \INT_l \intpr \INT_l}
\end{equation}
where $\ActS' = \cha^p_1:\STT_{1}^l, \dots, \cha^p_n:\STT^{l}_g, \cha^p_1:\que{}{\STT_{1}^l}, \dots \cha^p_n:\que{}{\STT^{l}_g}$ and by hypothesis $\ActS' \csub \ActS$. 
This concludes the analysis for this case.


\end{proof}



\subsection{Extension to the Asynchronous Case}
TBD

%\input{types.tex}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{A Compartmentalized Model of  Communication-Centric Applications}\label{s:arch}
\newcommand{\myapp}[4]{#1\big\langle #2 \,;\, #3\,;\, #4\big\rangle }
\newcommand{\stpar}{\diamond}
\newcommand{\appar}{\parallel}

The introduction of located processes and mechanisms for runtime adaptation defined over locations raises a natural question: how should  process specifications be organized in order to achieve modular treatment of adaptation events? In this section, we propose an architecture for communicating processes. 

%Let us define the syntax of our architecture:
%\begin{eqnarray*}
%Sys & = & A_1 \parallel \cdots \parallel A_n \parallel \mathcal{H} \parallel  \mathsf{Init} \\
%A_i& = & id\langle R \,, S\, , \mathcal{M} \rangle \\
%R & ::= & \scomponent{\locf{loc}}{!a(x).P}   \sepr \scomponent{\locf{loc}}{P^{-}}  \sepr R_1 \para R_2 \\
%S & ::= & \que{\cha^p}{\ST} \sepr \que{\locf{loc}}{\til{r}}
%\end{eqnarray*}
\subsection{Definition}
The syntax of processes considered in this section  
is a subset of that introduced in Table~\ref{tab:syntax}: 
\begin{eqnarray*}
P , Q & ::=  &   \nopenr{u@a}{x:\ST}.P  \sepr   \nopena{u}{x:\ST}.P  \sepr   \outC{\locf{loc}}{r}   \\
& \sepr &   \outC{k}{e}.P  \sepr   \inC{k}{x}.P
	\sepr   \select{k}{n};P  
   \sepr   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} 
    \sepr   \close{k}.P   \\
   & \sepr &  \mu \rv{X}.P  
	\sepr   \rv{X} 
  	\sepr   \ifte{e}{P}{Q}  
  	\sepr    P \para  P  	 
		\sepr    \restr{\cha}{P}   
	 \sepr   \restr{a}{P}   
	 \sepr   \mathbf{0}   
\end{eqnarray*}
Our set of processes 
is thus comparable to most session $\pi$-calculus, only extended with the adaptation request $\outC{\locf{loc}}{r}$.
Also, we consider a minor variation in the syntax of session requests, with a reference to an application $a$.
The need for reference will become clear later on. 
Let us assume the following abbreviations: 
\begin{eqnarray}
\ast\ift{cond}{P} & \triangleq & \mu \rv{X}.\ifte{cond}{P}{\rv{X}} \nonumber \\
\repopen{u}{x{:}\ST}.P & \triangleq & \mu \rv{X}.\nopena{u}{x{:}\ST}.(P \para \rv{X})  \nonumber
\end{eqnarray}
We write $P^{-}$ to denote the syntax of processes without service definitions $\nopena{u}{x{:}\ST}.P$.
As it will be clear later on, this is useful to isolate service definitions. 

Building upon processes, we now define our model of compartmentalized communicating systems. Before giving a formal definition, we offer an informal motivation.
Our model assumes that systems are deployed 
in a two-level scheme: from a global perspective, a system is an assembly of applications; 
local to each application, we have (located) processes (as introduced above) with their runtime state.
As we will see, some degree of communication between applications will be allowed.
In this way, a system corresponds to the composition of one or more \emph{applications}, denoted $A_1, A_2, \ldots$.
Each application has a unique identifier, denoted $a_1, a_2, \ldots$.
There are  \emph{handler} processes, denoted $\mathcal{H}_1, \mathcal{H}_2,  \ldots $, responsible for adaptation at the 
system (global) level: it may adapt a service definition at some specific applications, or it may affect a whole application.
%Also, there is an initialization process $\mathsf{Init}$ which starts the system by appropriately invoking applications.
Up to this point, we have:
\begin{eqnarray}
Sys & = &  A_1 \appar \cdots \appar A_n \appar \mathcal{H}_1 \appar \cdots \appar \mathcal{H}_k  \nonumber 
\end{eqnarray}
where `$\appar$' denotes the parallel composition operator at the system level. 

At the level of applications, we find three separate elements: the \emph{behavior} of the application, denoted $R$, which contains located service definitions and invocations; the \emph{state} of the application, denoted $\mathsf{S}$, which stores session and location queues associated to the behavior of the application, together with a queue for the application; and a \emph{manager} $\mathcal{M}$ which implements adaptation policies at the application (local) level. This scheme thus realizes the separation of concerns hinted at before.

More formally, our architectural model is defined by the following syntax.
We shall use $\locf{loc}, \locf{l}_1, \locf{l}_2, \ldots$ to range over locations. 
\begin{eqnarray*}
G & ::= & A \sepr \mathcal{H} \sepr G_1 \appar G_2 \\
A & :: = & \myapp{a}{R}{\mathsf{S}}{\mathcal{M}} \\
\mathcal{H} & ::= & *\,\ift{\arrive{\locf{loc}@a, \mathtt{upd}_E}}{\nadaptbig{\locf{loc}}{R}} \sepr *\,\ift{\arrive{a, \mathtt{upg}}}{\nadaptbig{a}{G}} \\
R & ::= & \scomponentbig{\locf{loc}}{\repopen{u}{x{:}\ST}.P}   \sepr \scomponentbig{\locf{loc}}{P^{-}}  \sepr R_1 \para R_2 \\
\mathsf{S} & ::= & \que{\cha^p}{\ST} \sepr \que{\locf{loc}}{\til{r}} \sepr \que{a}{\til{r}}  \sepr \mathsf{S}_1 \stpar \mathsf{S}_2 \\
\mathcal{M} & ::= & *\,\ift{\arrive{\locf{loc}, \mathtt{upd}_I}}{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}} \\
& \sepr & \mathcal{M}_1 \para \mathcal{M}_2 
\end{eqnarray*}
We write $G, G_1, G_2, \ldots$ to denote elements at the global (system) level. 
The intention is that a system is the parallel composition of a finite set of  
applications $A$ with some handlers $\mathcal{H}$. In essence, a handler is a persistent process which 
spawns an adaptation strategy as soon as an adaptation request arrives to an appropriate queue. It is worth noticing that 
this is the only part of our model in which update processes may occur. 
Handlers may adapt the behavior at some particular location included within an application. 
They may also upgrade a whole application. 
As mentioned above, applications represent a container in which communicating behaviors, 
their associated state, and related adaptation policies are jointly described. 
Indeed, the structure of applications enforces a separation between behavior and state, but also 
a separation with respect to adaptation policies. 
The behavior $R$ of an application consists of located processes: 
as before, locations are transparent; here we rule out their nesting, for simplicity. 
A design criteria in the specification of $R$ is the 
separation between located processes defining service definitions 
from the located processes which make use of such definitions.
Our operational semantics will ensure that locations enclosing service definitions do not contain open (active) sessions. 
This should be useful to better structure adaptation strategies, for service definitions may simply appeal to upgrades, without concerns of preservation of active sessions. The state $\mathsf{S}$ of an application collects the queues associated to the behavior contained: we consider queues for sessions and locations (as before) but also a queue for the whole application. We write $\mathsf{S}_1 \stpar \mathsf{S}_2$ to denote the parallel composition of two state elements (queues)  $\mathsf{S}_1$ and $\mathsf{S}_2$. Finally, managers $\mathcal{M}$ follow the same principles of handlers, but restricted to the setting of an application. In fact, it is worth noticing that managers may act upon the issue of an internal update request $\mathtt{upd}_I$ for some location, whereas handlers may act upon the arrival of an external update request or an application upgrade request (denoted $\mathtt{upd}_E$ and $\mathtt{upg}$, respectively).

%Notice that we separate the state of an application (its queues) so that handler $\mathcal{H}$ can restart an application by simply erasing the current state.
Overall, the our architecture defines a compartmentalized division the syntactic elements studied in previous sections.
With respect to adaptation, our model enforces  two different granularities: a global one, defined by the handler (which may update locations inside applications but also entire applications), and a local one, defined by the manager of each application (which may only update locations within his application). 

It is desirable to formally give reasonable conditions for forming systems. The following definition identifies a number of such conditions:

\begin{definition}
We will say that $G$ is a \emph{well-formed system} if it satisfies the following conditions:
\begin{enumerate}[(a)]
\item There is at least one application $A$ and one handler $\mathcal{H}$.
\item For each application $\myapp{a_i}{R_i}{\mathsf{S}_i}{\mathcal{M}_i}$ in $G$, 
state $\mathsf{S}_i$ contains exactly one application queue $\que{a_i}{\til{r}}$.
\item For each location $\locf{l}_j$ in $R_i$, there is exactly one location queue 
$\que{\locf{l}_j}{\til{r}}$ in $\mathsf{S}_i$ and 
exactly one associated  manager $\mathcal{M}_j$ is part of $\mathcal{M}_i$.
\item Every manager $\mathcal{M}_k$, part of $\mathcal{M}_i$, only refers to internal adaptation requests for location $\locf{l}_k$ occurring in $R_i$.
\end{enumerate}
\end{definition}

\subsection{Reduction Semantics}
Some selected rules are in Tables~\ref{tab:redsemari} and~\ref{tab:redsemarii}.
Rules for if and recursion are as for plain processes.

The semantics allows for remote session establishment: a service invocation can refer to a persistent service defined in an external application. Notice that this entails the code mobility of the requested services to the location of the callee.  
As a result, applications only store queues for sessions occurring in the application.

Need to re-define evaluation contexts. 
\begin{table}[t!]
$$
\begin{array}{lc}
\rulename{c:ROpen} & 
\myapp{a_1}{\scomponentbig{\locf{l}_1}{\repopen{u}{x{:}\ST}.P}}{\mathsf{S}_1}{\mathcal{M}_1} \appar  
\myapp{a_2}{\scomponentbig{\locf{l}_2}{\,\nopenr{u@a_1}{y{:}\overline{\ST}}.Q}}{\mathsf{S}_2}{\mathcal{M}_2} \vspace{-0.5mm}\\
&  \pired   \vspace{-0.5mm}\\
& \myapp{a_1}{\scomponentbig{\locf{l}_1}{\repopen{u}{x:\ST}.P}}{\mathsf{S}_1}{\mathcal{M}_1} \appar \\
& \myapp{a_2}{\scomponentbig{\locf{l}_2}{\restr{\cha}{( P\sub{\cha^+}{x} \para Q\sub{\cha^-}{y})}}}{
\mathsf{S}_2 \stpar 
\que{\cha^+}{\ST} \stpar 
\que{\cha^{-}}{\overline{\ST}}
}{\mathcal{M}_2} \vspace{3mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:LOpen} & 
\myapp{a_1}{\scomponentbig{\locf{l}_1}{\nopena{u}{x:\ST}.P} \para \scomponentbig{\locf{l}_2}{\nopenr{u}{y:\overline{\ST}}.Q}}{\mathsf{S}_1}{\mathcal{M}_1} \vspace{-0.5mm}\\
& \pired   \vspace{-0.5mm}\\
& %\hfill 
 \myapp{a_1}{\scomponentbig{\locf{l}_1}{\mathbf{0}} \para \scomponentbig{\locf{l}_2}{ \restr{\cha}{( P\sub{\cha^+}{x} \para Q\sub{\cha^-}{y})}}}{
\mathsf{S}_1 \stpar 
\que{\cha^+}{\ST} \stpar 
\que{\cha^{-}}{\overline{\ST}}
}{\mathcal{M}_1} \vspace{3mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:LOpen!} & 
\myapp{a_1}{\scomponentbig{\locf{l}_1}{\repopen{u}{x:\ST}.P} \para \scomponentbig{\locf{l}_2}{\nopenr{u}{y:\overline{\ST}}.Q}}{\mathsf{S}_1}{\mathcal{M}_1} \vspace{-0.5mm}\\
& \pired   \vspace{-0.5mm}\\
& 
 \myapp{a_1}{\scomponentbig{\locf{l}_1}{\repopen{u}{x:\ST}.P} \para \scomponentbig{\locf{l}_2}{ \restr{\cha}{( P\sub{\cha^+}{x} \para Q\sub{\cha^-}{y})}}}{
\mathsf{S} \stpar 
\que{\cha^+}{\ST} \stpar 
\que{\cha^{-}}{\overline{\ST}}
}{\mathcal{M}} 
\vspace{3mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:Com} &
 \myapp{a}{\scomponentbig{\locf{l}_1}{\outCn{\overline{\cha}^{\,p}}{v}.P \para \inC{\cha^{\,\overline{p}}}{{x}}.Q }}{
\mathsf{S} \stpar 
\que{\cha^p}{!(T).\ST} \stpar
\que{\cha^{\overline{p}}}{?(T).\overline{\ST}} 
}{\mathcal{M}}  \vspace{-0.5mm}\\
& \pired \vspace{-0.5mm}\\
& 
 \myapp{a}{\scomponentbig{\locf{l}_1}{P \para Q\subst{v}{x} }}{
\mathsf{S} \stpar 
\que{\cha^p}{\ST} \stpar \que{\cha^{\overline{p}}}{\overline{\ST}} 
}{\mathcal{M}}  
\vspace{3mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:Sel} &
 \myapp{a}{\scomponentbig{\locf{l}_1}{ \branch{\cha^{\,p}}{n_j{:}P_j}_{j \in J} \para  \select{\cha^{\,\overline{p}}}{n_j};Q   }}{
\mathsf{S} \stpar 
\que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}} \stpar
\que{\cha^{\overline{p}}}{\oplus\{n_j:\overline{\ST}_j \}_{j \in J}}
}{\mathcal{M}}  \vspace{-0.5mm} \\
& \pired \vspace{-0.5mm}\\
& 
 \myapp{a}{\scomponentbig{\locf{l}_1}{P_j \para Q}}{
\mathsf{S} \stpar 
\que{\cha^p}{\ST_j} \stpar \que{\cha^{\overline{p}}}{\overline{\ST}_j} 
}{\mathcal{M}}  \quad (j \in J)  
\vspace{3mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:Clo} &
 \myapp{a}{\scomponentbig{\locf{l}_1}{\close{\cha^{\,p}}.P    \para  
 \close{\cha^{\,\overline{p}}}.Q  }}{
\mathsf{S} \stpar 
\que{\cha^p}{\varepsilon} \stpar
\que{\cha^{\overline{p}}}{\varepsilon}
}{\mathcal{M}}  
 \pired 
 \myapp{a}{\scomponentbig{\locf{l}_1}{P \para Q}}{
\mathsf{S}  
}{\mathcal{M}}   
\end{array}
$$
\caption{Reduction Semantics for Architectures: Selected Rules (I) \label{tab:redsemari}}
\end{table}

\begin{table}[t!]
$$
\begin{array}{c}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:LPar1}]{P \pired P'}{ \myapp{a}{\scomponentbig{\locf{l}_1}{P \para R_1} \para R_2 }{
\mathsf{S}  
}{\mathcal{M}} \pired 
 \myapp{a}{\scomponentbig{\locf{l}_1}{P' \para R_1} \para R_2 }{
\mathsf{S}  
}{\mathcal{M}}
}
\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:LPar2}]{\mathcal{M} \pired \mathcal{M}'}{ \myapp{a}{R}{
\mathsf{S}  
}{\mathcal{M} \para \mathcal{M}_1} \pired 
 \myapp{a}{R}{
\mathsf{S}  
}{\mathcal{M}' \para \mathcal{M}_1}
}
%\vspace{2mm}\\
\qquad
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:GPar1}]{G \pired G'}{G \appar G_1 \pired G' \appar G_1}  
\vspace{2mm}\\
%\qquad
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\inferrule[ \rulename{c:Rec}]{}{ \recu\,\rv X. P \pired P\subst{\recu\,\rv X. P }{\rv X}}
%%\vspace{2mm}\\
%\qquad
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\inferrule[\rulename{c:IfTr}]{}{\ifte{\mathtt{true}}{P}{Q} \pired P }
%\vspace{2mm}\\
%%\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:UReq}]{}{
 \myapp{a}{\scomponentbig{\locf{l}_1}{~\outC{\locf{loc}}{r} \para R }}{
\mathsf{S} \stpar \que{\locf{loc}}{\til{r}_1} 
}{\mathcal{M}} \pired 
 \myapp{a}{\scomponentbig{\locf{l}_1}{ R }}{
\mathsf{S} \stpar \que{\locf{loc}}{\til{r}_1 \cdot r} 
}{\mathcal{M}}}
\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:GUpd1}]{}{\myapp{a}{R}{\mathsf{S}  }{\mathcal{M}} \appar \nadaptbig{a}{ \myapp{a}{R'}{\mathsf{S}'  }{\mathcal{M}'}} \pired \myapp{a}{R'}{\mathsf{S}'}{\mathcal{M}'} }
 \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:GUpd2}]{}{\myapp{a}{\scomponentbig{\locf{loc}}{P} \para R }{
\mathsf{S}  
}{\mathcal{M}} \appar \nadaptbig{\locf{loc}}{Q} \pired
\myapp{a}{\scomponentbig{\locf{loc}}{Q} \para R }{\mathsf{S}  }{\mathcal{M}} }
 \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:LUpd1}]{}{\myapp{a}{\scomponentbig{\locf{loc}}{P} \para R }{
\mathsf{S}  
}{\mathcal{M} \para \nadaptbig{\locf{loc}}{Q}}   \pired
\myapp{a}{\scomponentbig{\locf{loc}}{Q} \para R }{\mathsf{S}  }{\mathcal{M}} }
 \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:GArr1}]{}{\myapp{a}{R}{\mathsf{S} \stpar \que{a}{\til{r}}  }{\mathcal{M}} \appar \evc{E}[\arrive{a,r}]  \pired \myapp{a}{R}{\mathsf{S} \stpar \que{a}{\til{r}}  }{\mathcal{M}} \appar \evc{E}[\mathtt{b}] }
 \quad ((|\til{r}| \geq 1) \downarrow \mathtt{b}) 
 \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:GArr2}]{}{ \myapp{a}{R}{\mathsf{S} \stpar \que{\locf{loc}}{\til{r}}  }{\mathcal{M}} \appar \evc{E}[\arrive{\locf{loc}@a,r}]  \pired \myapp{a}{R}{\mathsf{S} \stpar \que{a}{\til{r}}  }{\mathcal{M}} \appar \evc{E}[\mathtt{b}] }
 \quad ((|\til{r}| \geq 1) \downarrow \mathtt{b}) 
 \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:LArr1}]{}{  \myapp{a}{R}{\mathsf{S} \stpar \que{\locf{loc}}{\til{r}}  }{\mathcal{M} \para \evc{E}[\arrive{\locf{loc},r}]}   \pired \myapp{a}{R}{\mathsf{S} \stpar \que{a}{\til{r}}  }{\mathcal{M} \para \evc{E}[\mathtt{b}] } }
 \quad ((|\til{r}| \geq 1) \downarrow \mathtt{b}) 
\end{array}
$$
\caption{Reduction Semantics for Architectures: Selected Rules (II)\label{tab:redsemarii}}
\end{table}



\subsection{Example}

Taken from~\cite{DBLP:conf/esorics/JiaAFBSFKM13}??

\section{Concluding Remarks}

\bibliographystyle{abbrv}
\bibliography{referen}
\end{document}

The report should contain the following information:
- purpose of the STSM;
- description of the work carried out during the STSM;
- description of the main results obtained;
- future collaboration with host institution (if applicable);
- foreseen publications/articles resulting or to result from the STSM (if applicable);
- confirmation by the host institution of the successful execution of the STSM;
- other comments (if any).


